Nuprl Lemma : es-when-init 11,40
es:event_system{i:l}, e:es-E(es), x:Id, T:Type.
es-dtype(es; loc(e); x; T)
 (es-when(es; x; es-init(es;e)) = es-initially(es; loc(e); x)  T) 
latex

Definitionsprop{i:l}, es-T(es), t.2, t.1, es_info(es), es-vartype(es; i; x), es-isconst(es; i; x), es_init(es), loc(e), es-E(es), es-initially(es; i; x), True, if b then t else f fi , tt, t  T, b, P  Q, x:A. B(x), constant_function(f; A; B), P  Q, es-dtype(es; i; x; T), event_system{i:l}, subtype(S; T)
Lemmases-time wf, int inc rationals, qadd wf, loc wf, assert wf, event system wf, es-E wf, Id wf, es-loc wf, es-dtype wf, es-loc-init, es-first-init, es-init wf, es-when-first

origin